Rubik’s Cube in Lean

This Github repo contains the proof that there are \(2^{12} \times 3^{8} \times 8! \times 11!\) Rubik’s cubes:

https://github.com/vihdzp/rubik-lean4

What! This is the most amazing thing I’ve read in a long time. What is the reason of this number? And it’s verified in Lean!!!